theory SimplTest
  imports "./lib/Simpl/Vcg" "./lib/Simpl/HeapList" Real
begin

hoarestate kstate = 
  A :: nat
  I :: nat
  N :: nat
  M :: nat
  R1 :: real
  R2 :: real


procedures Multi (N::nat, M::nat | R::nat)
  where I::nat in
    "\<acute>R :== \<acute>M * \<acute>N"



print_locale Multi_parameters_namespace
print_locale Multi_parameters_valuetypes
print_locale Multi_parameters

print_locale Multi_signature


print_locale Multi_variables_namespace
print_locale Multi_variables_valuetypes
print_locale Multi_variables

print_locale Multi_body

print_locale Multi_impl
print_locale Multi_clique

procedures TestMulti (N::nat, M::nat)
  where I::nat in
    "\<acute>I :== CALL Multi(\<acute>N,\<acute>M)"

print_locale TestMulti_parameters
print_locale TestMulti_variables

context TestMulti_signature
begin
declare [[hoare_use_call_tr' = false]]
term "CALL TestMulti(1,1)"
end

lemma (in Multi_impl) "\<forall>n m. \<Gamma>\<turnstile> \<lbrace>\<acute>M = m \<and> \<acute>N = n\<rbrace> \<acute>I :== CALL Multi(\<acute>N, \<acute>M) \<lbrace>\<acute>I = m * n\<rbrace>"
  by vcg simp

hoarestate globals_heap = 
  "next" :: "ref \<Rightarrow> ref"
  cont :: "ref \<Rightarrow> nat"
  p :: ref

procedures (imports globals_heap) 
  append(p :: ref, q :: ref | p :: ref)
    "IF \<acute>p = Null THEN \<acute>p :== \<acute>q
      ELSE \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q)
     FI"

print_locale append_impl

procedures (imports globals_heap)
  insert(r :: ref, p :: ref | p :: ref)
  "IF \<acute>r = Null THEN SKIP
   ELSE IF \<acute>p = Null THEN \<acute>p :== \<acute>r;; \<acute>p\<rightarrow>\<acute>next :== Null
         ELSE IF \<acute>r\<rightarrow>\<acute>cont \<le> \<acute>p\<rightarrow>\<acute>cont THEN
                  \<acute>r\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p :== \<acute>r
               ELSE \<acute>p\<rightarrow>\<acute>next :== CALL insert(\<acute>r,\<acute>p\<rightarrow>\<acute>next)
              FI
        FI
   FI
"

print_locale insert_impl
thm insert_body.insert_body_def

procedures (imports globals_heap)
  insertsort(p :: ref | p :: ref)
    where r :: ref q :: ref in 
    " \<acute>r :== Null;;
    WHILE(\<acute>p \<noteq> Null) DO
      \<acute>q :== \<acute>p;;
      \<acute>p :== \<acute>p\<rightarrow>\<acute>next;;
      \<acute>r :== CALL insert(\<acute>q,\<acute>r)
    OD;;
    \<acute>p :== \<acute>r"

definition (in insertsort_body) "call_insert p \<equiv> \<acute>p :== CALL insertsort(p)"

definition (in globals_heap) call_insert :: "ref \<Rightarrow> ref"
  where "call_insert p \<equiv> p"

print_locale insertsort_impl
print_locale insertsort_body
thm insertsort_body.insertsort_body_def
print_locale insertsort_body
thm insertsort_body.intro


context insertsort_signature
begin
declare [[hoare_use_call_tr' = false]]

end

lemma (in kstate) "\<Gamma>\<turnstile>\<lbrace>\<acute>R1 \<noteq> 0\<rbrace> \<acute>R2 :==\<^sub>g (\<acute>R2 + 1) div \<acute>R1 \<lbrace>True\<rbrace>"
apply vcg 
oops
  

end
